r:. ((r = 0  ))  ((r * 1/r) = 1  ) 

latex

Definitions	ff, tt, if b then t else f fi , (r/s), P & Q, , t  T, P  Q, qeq(r;s), P  Q, 1/r, r * s, P  Q, x:A. B(x), False, a  b  T , A c B, , x:A. B(x), A, S  T
Lemmas	rationals wf, not wf, assert of eq int, int nzero properties, q-elim, int inc rationals, qeq wf2, assert wf, not functionality wrt iff, qinv wf, qmul wf, assert-qeq